ma-frame-compat(A;B)
== adom((A.2.2.2).1). p=(A.2.2.2).1(a)   B.rframe(A.pre p for a)
== & kxdom((A.2.2.2.2).1). 

== ef=(A.2.2.2.2).1(kx)  
== efB.frame(kx.1 affects kx.2) & B.aframe(kx.1 affects kx.2) & B.rframe(A.effect ef of kx.1 on kx.2)
== & kldom((A.2.2.2.2.2).1). 

== & snd=(A.2.2.2.2.2).1(kl)  
== & snd(tg:Id. (tg  map(p.p.1;snd))  B.sframe(kl.1 sends <kl.2,tg>))
== & & B.bframe(kl.1 sends on kl.2)
== & & B.rframe(A.sends snd of kl.1 on kl.2) 

latex

---

clarification:

ma-frame-compat(A;B)
== IdIdDeqadom((A.2.2.2).1). p=(A.2.2.2).1(a)   B.rframe(A.pre p for a)
== & (:Knd  Id)product-deq(Knd;Id;KindDeq;IdDeq)kxdom((A.2.2.2.2).1). 

== ef=(A.2.2.2.2).1(kx)  
== efB.frame(kx.1 affects kx.2) & B.aframe(kx.1 affects kx.2) & B.rframe(A.effect ef of kx.1 on kx.2)
== & (:Knd  IdLnk)product-deq(Knd;IdLnk;KindDeq;IdLnkDeq)kldom((A.2.2.2.2.2).1). 

== & snd=(A.2.2.2.2.2).1(kl)  
== & snd(tg:Id. (tg  map(p.p.1;snd)  Id)  B.sframe(kl.1 sends <kl.2,tg>))
== & & B.bframe(kl.1 sends on kl.2)
== & & B.rframe(A.sends snd of kl.1 on kl.2) 

latex

Definitions	M.rframe(A.pre p for a), IdDeq, M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), xdom(f). v=f(x)   P(x;v), x:A  B(x), product-deq(A;B;a;b), Knd, IdLnk, KindDeq, IdLnkDeq, P & Q, x:A. B(x), P  Q, (x  l), map(f;as), x.A(x), Id, M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), t.1, t.2
FDL editor aliases	ma-frame-compat